import {promises as fs} from "fs";
import chalk from 'chalk';
import fg from 'fast-glob';

// import * as readline from 'node:readline/promises';
// import { stdin as input, stdout as output } from 'node:process';

// const rl = readline.createInterface({ input, output });

var Bin = (function() {
  var upperRef;
  var upperPol;
  
  const bg = {
     "0": chalk.bgGreenBright,
    "00": chalk.bgGreenBright,
     "1": chalk.bgBlue,
    "10": chalk.bgRed,
    "11": chalk.bgBlue
  };

  const fg = {
     "0": chalk.greenBright,
    "00": chalk.greenBright,
     "1": chalk.blue,
    "10": chalk.red,
    "11": chalk.blue
  };

  return {

    logR(width, ref) {

      if (ref === undefined) {
        if (upperRef !== undefined) {
          for (let i = 1; i < width + 1; i ++) process.stdout.write(chalk.black(bg[upperRef[i]]("▄"), ""));
          process.stdout.write("\n");
          upperRef = undefined;
        }
        return;
      } else {
        const refStr = ref.toString(2).padStart(width+1, 0).split("").reverse().join("");

        if (upperRef) {
          for (let i = 1; i < width + 1; i ++)
          process.stdout.write(chalk.black(bg[upperRef[i]](fg[refStr[i]]("▄"), "")));
          process.stdout.write("\n");
          upperRef = undefined;
        } else {
          upperRef = refStr;
        }
      }
    },

    logRP(width, [ref, pol]=[]) {
      if (ref === undefined) {
        if (upperRef !== undefined) {
          for (let i = 1; i < width + 1; i ++) process.stdout.write(chalk.black(bg[upperRef[i] + upperPol[i]]("▄"), ""));
          process.stdout.write("\n");
          upperRef = undefined;
          upperPol = undefined;
        }
        return;
      } else {
        const refStr = ref.toString(2).padStart(width+1, 0).split("").reverse().join("");
        const polStr = pol.toString(2).padStart(width+1, 0).split("").reverse().join("");

        if (upperRef) {
          for (let i = 1; i < width + 1; i ++)
          process.stdout.write(chalk.black(bg[upperRef[i] + upperPol[i]](fg[refStr[i] + polStr[i]]("▄")), ""));
          process.stdout.write("\n");
          upperRef = undefined;
          upperPol = undefined;
        } else {
          upperRef = refStr;
          upperPol = polStr;
        }
      }
    }
  }
})(); 

function ws(text) {
  for (let i = 0; i < text.length; i++)
    if (text[i] === 32 || text[i] >= 9 && text[i] <= 13) continue;
    else return text.slice(i);
  return new Uint8Array(0);
}

function newLine(text) {
  for (let i = 0; i < text.length; i++)
    if (text[i] == '\n'.charCodeAt(0)) return text.slice(i + 1)
  return new Uint8Array(0);
}

function num(text) {
  var int = 0;
  var sgn = 1;

  text = ws(text);
  let dex = 0
  for (; dex < text.length; dex++) 
    if (text[dex] === '-'.charCodeAt(0)) sgn = -1;
    else if (text[dex] >= 48 && text[dex] <= 57) int = int * 10 + (text[dex] - 48);
    else break; 

  return {
    num: int * sgn,
    res: text.slice(dex)
  }
}

var Sol = (function() {

  const enc = new TextEncoder();
  const dec = new TextDecoder();
  const {ceil, trunc, sign:sgn, abs} = Math;

  var tab = new Map();
  var stats = {};
  var width = undefined;
  var lines = undefined;

  function log () {
    Bin.logRP(width);
    for (let ref of tab.keys()) for (let pol of tab.get(ref)) Bin.logRP(width, [ref, pol]);
    Bin.logRP(width);
  }

  function cnf (text) {

    var pols = 0n;
    var refs = 0n; 
    while (text.length > 0) {
      text = ws(text);
      if (text.length == 0 || text[0] === 37) break;

      switch(String.fromCharCode(text[0])) {
        case 'c': text = newLine(text); break;
        case 'p': if (dec.decode(text.slice(0, 5)) == "p cnf") {
          text = text.slice(5);
          ({num: width, res:text} = num(text));
          ({num: lines, res:text} = num(text));

          // console.log(width, lines);

          stats.pos = Array(width + 1).fill(0n);
          stats.neg = Array(width + 1).fill(0n);
        }
          break;
        default: {
          var {num: lit, res:text} = num(text);
          if (text[0] == 0 && lit != 0) throw Error("CNF: unexpected EOF");
          if (lit != 0) {
            const pol = sgn(lit) > 0 ? 1n : 0n;
            const pos = BigInt(abs(lit));
            refs |= 1n << pos;
            pols ^= (-pol ^ pols) & (1n << pos);
          } else {
            // console.log(lit, dec.decode(text));
            // const c = [refs, pols];
            // Bin.logRP(width, [refs, pols]);
            tab.has(refs) 
              ? tab.get(refs).add(pols)
              : tab.set(refs, new Set([pols]));
            // tab.push(c);
            pols = 0n;
            refs = 0n;
          }
        } 
      }
    }

    // Bin.logRP(width);
    return width;
  }

  // heuristically find nex variable to be eliminated
  function nex() {
    const pos = Array(width + 1).fill(0n);
    const neg = Array(width + 1).fill(0n);
    for (const [ref, pols] of tab) for (const pol of pols){
      let r = ref, p = pol;
      for (let d = 0; r; r >>= 1n, p >>= 1n, d++) {
        pos[d] += r & p & 1n;
        neg[d] += r & (~p & 1n);
      }
    }
    let min = undefined;
    let dex = 0;
    let arr = [];
    for (let i = 1; i < width + 1; i++) {
      const inc = pos[i] * neg[i] - (pos[i] + neg[i]);
      arr.push(inc);
      if (min === undefined) {
        min = inc;
        dex = 1;
      } else if (min > inc) {
        min = inc;
        dex = i;
      }
    }
    // console.log(chalk.bold.blue("NEX"), `ESTIMATED INCREMENT ${chalk.bold(min)} @ POS ${chalk.bold(pos[dex])} NEG ${chalk.bold(neg[dex])}`);
    return {dex, min};
  }

  /**
    * overwritting the given bit with width bit, and reset the width bit.
    * @param {BigInt}  num: the given number, can be either reference or polarity
    * @param {Integer} dex: the index to be overwritten
    *
    * Note: Not to confuse the MSB and "width bit" referred here. the width bit
    *       means the bit over the width-th bit. while MSB refer to the bit where
    *       the leftmost one lies at.
    */
  function swp(num, dex) {
    const colN = BigInt(width);
    const dexN = BigInt(dex);
    const xor = ((num >> dexN) ^ (num >> colN)) & 1n; // XOR temporary
    num ^= (xor << dexN) | (xor << colN);
    num &= ~(1n << colN);
    return num;
  }

  function swpAll(dex) {
    const dexN = BigInt(dex);
    const colN = BigInt(width);
    const nexab = new Map();
    for (let [ref, pols] of tab) {

      // console.log('here', ref)
      // 4.1. remove the original ref and associated pols
      tab.delete(ref);

      const nexPols = []
      for (const pol of pols)
        nexPols.push(swp(pol, dex));

      nexab.set(swp(ref, dex), new Set(nexPols));
    }
    width -= 1;
    tab = nexab;
  }

  function log2(n) {
    let d = 0;
    while (n >>= 1n) d++;
    return d;
  }

  function uni() {
    prop: while(1) {
      for (const [ref, pols] of tab) { 
        if ((ref !== 0n) && (ref & (ref - 1n)) === 0n) {
          const pol = [...pols][0];

          // console.log(chalk.yellow.bold("UNI", "FOUND"))
          
          for (const [refM, polsM] of tab) if ((refM & ref) === ref) {
            const polsMnew = [...polsM]
              .filter(p => !(~(p ^ pol) & ref))  // remove all clauses containing literals with same polarity
              .map(p => p & ~ref);                // reset the literal bit for remaining clauses
            tab.set(refM, new Set(polsMnew));
          } 
          swpAll(log2(ref));
          continue prop;
        }
      }
      break;
    }

  }

  function res(lim=65536) {

    const {dex, min} = nex();


    // 1. Find all clauses containing the variable to be eliminated
    //    By adding the clauses into pos and neg set, the variable
    //    slot is cleared for deendining tautology later on.
    const pos = [];
    const neg = [];
    const non = new Map();
    const neu = [];
    const mas = BigInt(1 << dex);
    for (const [ref, pols] of tab) if (ref & mas) {

      // 1.1 remove the variable bit, put into pos/neg bins respectively.

      for (const pol of tab.get(ref)) {
        // 1.1 remove the variable bit
        const elem = [ref & ~mas, pol & ~mas];

        // 1.2 add the ref/pol pair into corresponding pos/neg list
        (pol & mas) ? pos.push(elem) : neg.push(elem);
      }

      // 1.2. remove the original ref key since it doesn't exist anymore.
      tab.delete(ref);
    } else {

      // 1.3 move the remaining refs into non for furture use of subsumption.
      non.set(ref, pols);
    }

    // if (pos.length > 1024 || neg.length > 1024) {
    //   if (pos.length > 1024) {
    //     console.log("P")
    //     pos.sort(([rA, pA], [rB, pB]) => rA === rB ? pA - pB : rA - rB);
    //     const pp = pos.slice()
    //     Bin.logRP(width);
    //     for(const p of pos) Bin.logRP(width, p)
    //     Bin.logRP(width);
    //     return 30;
    //   } else if (neg.length > 1024) {
    //     console.log("N")
    //     neg.sort(([rA, pA], [rB, pB]) => rA === rB ? pA - pB : rA - rB);
    //     Bin.logRP(width);
    //     for(const n of neg) Bin.logRP(width, n)
    //     Bin.logRP(width);
    //     console.log(non.size);
    //     return 30;
    //   }
    // }

    // console.log("2", pos, neg)
    // 2. Applying Resolution 
    
    let inc = 0;
    let tot = 0;
    let sub = 0;
    if (pos.length > 0 && neg.length > 0) for (let [refP, polP] of pos) for (let [refN, polN] of neg) {

      let jmp = 0;

      // 2.1. eliminating tautology
      // A: refP & refN: the bits shared by two refs
      // B: polP ^ polN: the bits that has different polarity
      // A & B: the bits that has different polarity and both clause has the lit.
      if (refP & refN & (polP ^ polN)) {
        tot++;
        jmp++ ;
      }

      const refU = refP | refN;
      const polU = polP | polN;

      // 2.2 check if subsumed
      if (!jmp) {
        for (const [ref, pols] of non) if ((refU & ref) === ref) if (pols.has(polU & ref)) {
          sub++;
          jmp++;
          break;
        }
      }
      
      // 2.2. pushing the resolvent clauses
      // console.log(tab.get(refP | refN));
      if (!jmp){
        inc ++;
        tab.has(refU)
          ? tab.get(refU).add(polU)
          : tab.set(refU, new Set([polU]));
      }
    }
    // console.log(chalk.bold.cyan("RES"), "ACTUAL INCREMENT   ", chalk.bold(inc), "TOT:", chalk.bold(tot), "SUB:", chalk.bold(sub));
    process.stdout.write(`${inc} `);

    // 4. Width Reduction
    //    swap the MSB column to the eliminated column, and reduce the width
    swpAll(dex); 
    // console.log()
    // log();
    return 0;
  }


  // Subsumption
  // For test each group of clauses which share same occurrence vector. For
  // a new tested occur vec "ref", if codex includes any pattern pat that,
  // ref & pat == pat, then 
  
  function subPol(sups, subs, subPatt) {
    let n = 0;
    for (const sup of sups) if (subs.has(subPatt & sup)) {
      sups.delete(sup);
      n++;
    }
    return n;
  }

  function sub() {
    const pat = new Map();
    var dec = 0;
    n:for (const [tabRef, tabPols] of tab) {
      for (const [patRef, patPols] of pat) {

        if ((patRef & tabRef) === patRef) {
          // if occur vec seems to be subsumable
          dec += subPol(tabPols, patPols, patRef);
          
          // The ref entry will be removed from the grand tab if all clause
          // are subsumed.
          if (tabPols.size === 0) tab.delete(tabRef);
          continue n;

        } else if ((patRef & tabRef) === tabRef) {
          // if occur vec can be subsumed by ref
          // same polarity level subsumption check
          // for (const patPol of patPols) if (pols.has(ref & patPol)) patPols.delete(patPol);
          dec += subPol(patPols, tabPols, tabRef);

          // replace the the pattern with ref in pat.
          pat.delete(patRef);

          // sine patRef must be in the tab and added into the pat,
          if (patPols.size === 0) tab.delete(patRef);
        }
      }
      // if ref was not subsumed by any ref pattern in pat, add it to the pat
      pat.set(tabRef, tabPols);
    }
    // for (const code of pat) Bin.logR(width, code);
    // console.log(pat.size, tab.size, dec);
    // console.log(chalk.bold.magenta("SUB"), `SUBSUMED            ${chalk.bold.redBright(dec)}`);
  }

  function end() {
    if (tab.size === 0) return 10;
    for (const [ref] of tab) if (!ref) return 20;
    return 0;
  }

  return {cnf, uni, res, sub, end, log};
})();

(async () =>{
  const paths = await fg('./cnf/uf20/*')
  paths.sort()

  for (const p of paths) {
    console.log("FILE", p);
    try {
      const data = await fs.readFile(p);

      // data is a Buffer that can be directly converted to a Typed Array
      const buf = new Uint8Array(data.buffer, data.byteOffset, data.byteLength);
      var width = Sol.cnf(buf); 
      
      var res;
      var iter = 0;
      const resV = {
        10: 'S SATIS',
        20: 'S UNSAT',
        30: 'S ERROR'
      }
      while(1) {
        // console.clear();
        // console.log(`\nVAR ${chalk.whiteBright.bold(iter++)}\n`);
        // if (res = Sol.uni()) break;
        if (res = Sol.end()) break;
        if (res = Sol.res(1048576)) break; 
        Sol.sub();
      }
      console.log(resV[res]);
      // Sol.log();
    } catch (err) {
      console.error('Error reading the file:', err);
    }
  }

})()
